@$i$ (with ds: ${\it ds}$ action $a$:$T$ precondition $a$ is $P$ s)($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$) then (precondition $a$:Outcome($T$) is $P$:State(${\it ds}$) {-}$>$ Bool) else  fi